state_after(e)
== state_after(e;e.w-info(w;e);e.w-pred(w;e);i,x. s(i;0).x;i.1of(2of(w-machine(w;i)));e.
== val(e)) 

latex

---

clarification:

w_state_after(w;e)
== state_after(e;e.w-info(w;e);e.w-pred(w;e);i,x. w-s(w; i; 0; x);i.1of(2of(w-machine(w;i)));e.
== w-eval(w; e)) 

latex

Definitions	state_after(e;info;pred?;init;Trans;val), w-info(w;e), w-pred(w;e), s(i;t).x, #$n, 1of(t), 2of(t), w-machine(w;i), x.A(x), val(e)
FDL editor aliases	w_state_after